T:Type, P:(T), L:T List. filter(P;L) = filter2(i.P(L[i]);L)  T List 

latex

Definitions	x:A. B(x), ||as||, t  T, ij, {i..j}, P  Q, l[i], filter2(P;L), Prop, b, A, b, , P & Q, P  Q, Unit, hd(l), i<j, ij, if b t else f fi, P  Q, True, T, AB
Lemmas	select cons tl, squash wf, le wf, cons filter2, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf, filter2 wf, select wf, int seg wf, length cons, non neg length, length wf1